A:Type, d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 

latex

Definitions	Unit, Prop, b, b, , P  Q, false, A, False, P  Q, P & Q, P  Q, true, EqDecider(T), x:A. B(x), t  T, eqof(d)
Lemmas	deq wf, bool sq, bool wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert